package de.fuberlin.inf.alp3.ue05;

public class BooleanStack implements Stack<Boolean> {
    // model: s :: unsigned int (32 bits)
    // inv: (log_2 s) < 32 (length s <= 31)
    private int value = 1;
    
    @Override
    public int length() {
        // pre:     --
        // post:    result = floor (log_2 s) 
        return 0;
    }
    @Override
    public Boolean pop() throws StackUnderflow {
        // pre:     s > 1 (length s >= 1)
        // post:    s' = s / 2 && (result = (s % 2 == 1))
        return null;
    }
    @Override
    public void push(Boolean b) throws StackOverflow {
        // pre:     length s < 31 -- else Overflow
        // post:    s' = s * 2      for b == false
        //          s' = s * 2 + 1  for b == true
        //          (=> length s' = length s + 1)
    }
}